$\forall$$T$:Type, $a$, $b$, $c$:($T$ List). \\[0ex]l\_disjoint($T$;$b$ @ $c$;$a$) $\Leftarrow\!\Rightarrow$ (l\_disjoint($T$;$b$;$a$) \& l\_disjoint($T$;$c$;$a$))